Decidable and Undecidable Fragments of Asynchronous Subtyping for Session Types

摘要

Session types are behavioural types for guaranteeing that some programs arefree from basic communication errors. Recent work has shown that the notion ofasynchronous subtyping for session types is undecidable. However, it is notclear what the possible alternatives for making such relation decidable are. Inthis work, we propose two algorithms for deciding restricted but practicallyrelevant definitions of asynchronous subtyping. Additionally, we further refinethe existing undecidability results by showing how two restricted forms ofasynchronous subtyping remain undecidable.